L:( List), a:. (0 < ||L||)  ((imax-list(L)  a)  (bL. b  a)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, A  B, imax-list(L), {T}, t  T, Top, S  T, , Y, P & Q, P  Q, A, False, x. t(x), list_accum(x,a.f(x;a);y;l), hd(l), tl(l), i  j , , ||as||, x(s)
Lemmas	nat wf, length wf nat, top wf, length wf1, le wf, imax-list wf, length wf2, l all wf2, l member wf, iff functionality wrt iff, l all cons, l all nil, imax wf, length cons, non neg length, and functionality wrt iff, guard wf, imax lb, nat properties, ge wf